#######################################################
# Example of FRTDEVS network modified from the monorail 
# system introduced in MH Hwang and BP Zeigler, 
# "Reachability  Graph of Finite and Deterministic DEVS 
# Networks",  IEEE Trans. on ASE, V6, N3, Jul, 2009, 
# pp468-478.
#  
# Author: moonho.hwang@gmail.com
#   Date: Oct.19.2011
#######################################################

from XSY.DEVS.FRTDEVS import * 
from XSY.DEVS.CoupledDEVS import *
from XSY.Set.Interval import *
from XSY.DEVS.SimEngine import SimEngine
from XSY.DEVS.VeriEngine import VeriEngine
import string

class Station(FRTDEVS):
   '''an atomic FRTDEVS for a station'''
   def __init__(m, n, phase0, vid, nso, tll, tlu, parent=None):
      '''constructor'''
      FRTDEVS.__init__(m, n, parent) 
      m.addInputPorts('?p', '?v', '?a')
      m.addOutputPorts('!v')
      m.phase0 = phase0
      m.vid0 = vid
      m.nso0 = nso
      m.tll = tll
      m.tlu = tlu

   def get_state(m):
      '''get the state'''
      return (m.phase, m.vid, m.nso)

   def set_state(m, s):
      '''set the state as s'''
      m.phase, m.vid, m.nso = s
 
   def delta_0(m):
      '''initial state'''
      m.phase, m.vid, m.nso = m.phase0, m.vid0, m.nso0

   def rv_tau(m):
      '''lifespan range function'''
      if m.phase == 'L':
         return TInterval(m.tll,m.tlu) # continuous random variable distributed uniformly 
      elif m.phase == 'S':
         return TInterval(5,5)
      else: # C and W
         return float('inf') # discrete random variable

   def delta_x(m, x):
      '''external transition function'''
      if x.port == m.IP['?v']: # vehicle 
         m.vid = x.value 
         if m.phase == 'E':
            rho = True; m.phase = 'L' # Loading
         else:
            rho = True; m.phase = 'C' # Collision
      elif x.port == m.IP['?p']: # pull signal
         m.nso = False # next station become empty
         if m.phase == 'W':
            rho = True; m.phase = 'S'; 
	    #########################################################################
            m.nso = True #set next station is occupied(intensional comment out)
         else:
            rho = False;
      elif x.port == m.IP['?a']:
         if m.phase == 'W':
            rho = True; 
            m.phase = 'L'; # Loading again because of passengers arrival
         else: # if not W, ignore the ?a signal
            rho = False

      return rho 
          
   def delta_y(m):
      '''output and internal transition function'''
      if m.phase == 'L':
         y = None
         if m.nso == False:
            m.phase = 'S'
	    ##########################################################################
            m.nso = True # set next station occupied.(intensional comment out)
         else:
            m.phase = 'W'
         return  y
      elif m.phase == 'S':
         y = PortValue(m.OP["!v"],m.vid)
         m.phase = 'E'
         return  y
      else:
         raise Exception ("How can we get here! phase = %s of %s."%(str(m.phase), hiername(m)))

def make_input_event(md):
   ''' a callback function for injection'''
   ipn = raw_input('input port name>')
   if ipn in md.IP:
      ip = md.IP[ipn]
      return PortValue(ip)
   else:
      return None # inject None into timer 

def makeModel(name, no_sts, no_vhc):
   '''make the monorail system: with the no of stations no_sts, and no of vehicles no_vhc'''
   cm = CoupledDEVS(name, None)
   prev_st = None
   # i is the station index 
   for i in range(1,no_sts+1):
      cm.addInputPorts("?a"+str(i))

      if i % 2: tl,tu = 20,22
      else:     tl,tu = 40,42

      if i < no_vhc:
         st = Station("s"+str(i), 'L', i, True, tl,tu)
      elif i == no_vhc:
         st = Station("s"+str(i), 'L', i, False, tl,tu)
      elif i < no_sts:
         st = Station("s"+str(i), 'E', 0, False, tl,tu)
      else:
         st = Station("s"+str(i), 'E', 0, True, tl,tu)

      cm.addComponents(st)
      cm.addCouple(cm.IP["?a"+str(i)], st.IP["?a"])

      if prev_st != None: # previous station exists
         cm.addCouple(prev_st.OP["!v"],   st.IP["?v"])
         cm.addCouple(st.OP["!v"],   prev_st.IP["?p"])

      if i == 1:
         st0 = st

      if i == no_sts:
         cm.addCouple(st.OP["!v"],  st0.IP["?v"])

	 ##<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
         cm.addCouple(st0.OP["!v"],  st.IP["?p"]) # comment out for non-live system test

      prev_st = st

   return cm

def runSimulation(md):
   '''run a simulation thread'''
   engine = SimEngine(md1, make_input_event)

   #---- setting StepByStep and DES simulation only ----
   #engine.StepByStep = True
   engine.sfactor = float('inf')
   #----------------------------------------------------
   engine.runInteractiveMenu()

def deadLock(ReachG):
   '''check if v is dead'''
   flag = False
   for v in ReachG.V:
      for n in v.s:
	 if v.s[n][0][0] == 'C':# the  first [0]: discrete state s, [1] lifetime ts (see XSY\DEVS\ReachGen.py)
	                        # the second [0]: phase (see get_state(m))
            print '%s is a dead state'%str(v)
            flag = True
   return flag


def livenessCB(KDAG):
   '''check if sc is alive'''
   for k in KDAG.V:
      sc = KDAG.kv[k] # for each vertex cv in KDAG.V
      if len(sc)>1: # multiple vertex in it
         model_E = {} # check model n true for having 'E' state
	 model_S = {} # check model n true for having 'S' state
         for v in sc: # for each vertex v in sc
            for n in v.s: # for each model n in v
               if n not in model_E: model_E[n] = False # initialization
               if n not in model_S: model_S[n] = False # initialization
               if v.s[n][0][0] == 'E': # the  first [0]: discrete state s, [1] lifetime ts (see XSY\DEVS\ReachGen.py)
	                               # the second [0]: phase (see get_state(m))
                  model_E[n] = True 
               elif v.s[n][0][0] == 'S':# the first [0]: discrete state s, [1] lifetime ts (see XSY\DEVS\ReachGen.py)
	                                # the second [0]: phase (see get_state(m)) 
                  model_S[n] = True
         all_meet = True
         for n in model_E:
            if not(model_E[n] and model_S[n]):
               all_meet = False
               break
         if all_meet:
            return True
   return False

def runVerification(md, no_sts):
   '''run a verification engine for the model md'''
   X = []
   for i in range(1, no_sts+1):
      ipstr = "?a"+str(i)
      ip = PortValue(md.IP[ipstr])
      if ip: X.append(ip)
      else:
         print "%s doesn't have ip port %s."%s(md.name, ipstr)
 
   VE = VeriEngine(md, X, deadLock, livenessCB)
   VE.runtimeInteractiveMenu()

if __name__ == '__main__':
   no_sts = no_vhc = 0
   while not (no_sts > no_vhc and no_sts > 0 and no_vhc):
      no_sts = string.atoi(raw_input("how many stations>"))
      no_vhc = string.atoi(raw_input("how many vehicles>"))

   md1 = makeModel("", no_sts, no_vhc) 

   c = True
   while c:
      s = raw_input('[s]im, [v]eri, e[x]it>')
      if s == 's' or s == 'sim': 
         runSimulation(md1)
      elif s == 'v' or s == 'veri':
         runVerification(md1, no_sts)
      elif s == 'x' or s == 'exit':
         c = False
      else:
         print('%s is an invalid input!'%s)
      
   print "good bye~!" 
  
